from deslab import *
    
def is2controllable(H,G):
    dump = 'D'
    Sigma_uc = G.E - G.Econ 
    G_pc = G.pfclosed()
    H_pc = H.pfclosed()
    Haug = H_pc.copy()    
    Haug = Haug.addstate(dump, mark='marked')
    
    for state in H_pc.X:
        for event in (Sigma_uc - H_pc.gamma(state)):
            Haug = Haug.addtransition([state,event,dump])   
    L = Haug & G_pc    
    if L<= H_pc:
        return True
    else:
        return False  
       
#def supconsublang(G,H):
#    Sigma_uc = G.E-G.con
#    H0 = H.trim()
#    H0 = H0&G
#    for state in H0:
#        y,x = state
#        if G.gamma(x) &     

def islangcontrollable(H,G):
    controllable = True
    Sigma_uc = G.E-G.Econ
    H0 = product(H,G,'tuple')   
    for (y,x) in H0.X:
        G_events_uc =  G.gamma(x)&Sigma_uc
        if not H0.gamma((y,x)) >= G_events_uc :
            controllable = False
    return controllable


def supcontrollable(H,G):
    Sigma_uc = G.Sigma-G.Sigcon
    H0 = H&G    
    H_last = fsa()
    while ((H0 <> H_last)&(H0<> fsa())):
        H_last = H0
        for (y,x) in H0.X:
            G_events_uc =  G.Gamma(x)&Sigma_uc
            if not(G_events_uc <= H0.Gamma((y,x))):
                H0 = H0.deletestate((y,x))                          
        H0 = trim(H0)

    return H0
   
                     
    




# Exmaple 1
#a1,b1,a2,b2,s0,s1,s2,s3,s4,s5,s6,s7  = definesymbols('a_1 b_1 a_2 b_2 0 1 2 3 4 5 6 7')
#XG=[s0,s1,s2,s3]
#XH = [s0,s1,s2,s3,s4,s5,s6,s7]
#sigma = [a1,b1,a2,b2]
#X0 = [s0]
#Xmh = [XH]
#
#transition_G = [[s0,a1,s1],[s1,a2,s3],[s3,b1,s2],[s2,b2,s0],
#            [s0,a2,s2],[s2,a1,s3],[s3,b2,s1],[s1,b1,s0]]
#transition_H = [[s0,a1,s1],[s0,a2,s4],[s1,b1,s2],[s1,a2,s5],[s2,a1,s3],[s2,a2,s6],[s3,a2,s7],
#            [s4,b2,s0],[s4,a1,s5],[s5,b2,s1],[s5,b1,s6],[s6,a1,s7],[s6,b2,s0],[s7,b2,s1]]
#sigmacon=[a2,b2]
#G=fsa(XG,sigma,transition_G,X0,XG,Econ = sigmacon,name='$G$') 
#H=fsa(XH,sigma,transition_H,X0,XH,Econ = sigmacon,name='$H$')
#H = H.pfclosed()

#Example 2
#a,b,u,s1,s2,s3,s4 = definesymbols('a b u 1 2 3 4')
#XG = [s1,s2,s3,s4]
#XH = [s1,s2,s3,s4]
#Sigma = [b,u]
#Xm,X0 = [s4,s3],[s1]
#trans_G = [[s1,u,s2],[s2,b,s4],[s1,b,s3],[s3,u,s4]]
#trans_H = [[s1,u,s2],[s2,b,s4],[s1,b,s3]]
#Sigmacon=[b]
#G=fsa(XG,Sigma,trans_G,X0,Xm,Econ = Sigmacon,name='$G$') 
#H=fsa(XH,Sigma,trans_H,X0,Xm,Econ = Sigmacon,name='$H$')
#H1=H.copy()


#Exmaple 3.3 Kassandras

# automata definition 
#a1,b1,a2,b2,s0,s1,s2,s3,s4,s5,s6,s7,s8,s9 = definesymbols('a_1 b_1 a_2 b_2 0 1 2 3 4 5 6 7 8 9')
#X_G = [s0,s1,s2,s3,s4,s5,s6,s7,s8]
#Xm=[s8]
#X0=[s0]
#Sigma = [a1,b1,a2,b2]
#Sigmacon = [a1,b1] 
#X_H = X_G+[s9]
#T_G = [(s0,a1,s1),(s0,a2,s3),(s1,b1,s2),(s1,a2,s4),(s2,a2,s5),(s3,a1,s4),
#       (s3,b2,s6),(s4,b1,s5),(s4,b2,s7),(s5,b2,s8),(s6,a1,s7),(s7,b1,s8)]
#T_H = [(s0,a1,s1),(s0,a2,s3),(s1,b1,s2),(s1,a2,s9),(s2,a2,s5),(s3,a1,s4),
#       (s3,b2,s6),(s9,b1,s5),(s4,b2,s7),(s5,b2,s8),(s6,a1,s7),(s7,b1,s8)]
#G = fsa(X_G,Sigma,T_G,X0,Xm,Econ = Sigmacon, name='$G$') 
#H = fsa(X_H,Sigma,T_H,X0,Xm, name='$H$')
#
##draw(G,H)
#
##
#test1 = islangcontrollable(H,G) 
#print test1
#Ksup = supcontrollable(H,G)
#test2 = islangcontrollable(Ksup,G) 
#print test2
#draw(G,H,Ksup)


#print test1 , test2#draw(R)
#SupCon.type='supervisor'
#print 'H is controllable is',test1,'-SupCon is controllable is' ,test2
#draw(G,H,Ksup)
##X1=[s1,s2,s3,s4,s5,s6,s7]


#a1,b1,a2,b2,s0,s1,s2  = definesymbols('a_1 b_1 a_2 b_2 0 1 2')
#XG=[s0,s1,s2]
#XH = XG+[s9]
#sigma = [a1,b1,a2,b2]
#X0 = [s0]
#XmH, XmG = [s8],[s8]
#sigmacon = [a1]
#trans_G = [[s0,a1,s1],[s0,a2,s3],[s1,b1,s2],[s1,a2,s4],[s2,a2,s5],
#           [s3,a1,s4],[s3,b2,s6],[s4,b1,s5],[s4,b2,s7],[s5,b2,s8],
#           [s6,a1,s7],[s7,b1,s8]]
#trans_H = [[s0,a1,s1],[s0,a2,s3],[s1,b1,s2],[s1,a2,s9],[s2,a2,s5],
#           [s3,a1,s4],[s3,b2,s6],[s9,b1,s5],[s4,b2,s7],[s5,b2,s8],
#           [s6,a1,s7],[s7,b1,s8]]
#
#G=fsa(XG,sigma,trans_G,X0,XmG,Econ = sigmacon,name='$G$',type='plant') 
#H=fsa(XH,sigma,trans_H,X0,XmH,Econ = sigmacon,name='$H$',type='specification')
#
#
#test=iscontrollable(H,G) 
#print test
#R=supcontrollable(H,G)
#test=iscontrollable(R,G) 
#draw(R)


# exemplo clasico

syms('a b c d e q0 q1 q2')
#table1 = [(q0,'q_0'),(q1,'q_1'),(q2,'q_2')]
X_12 = [q0,q1]
X3 = [q0,q1,q2]
Xm =[q0]
X0 = [q0]
Sigma1 = [a,b]
Sigma2 = [c,d]
Sigma3 = [b,c,d,e]
Sigma4 = [b,c,e]
T1 = [(q0,a,q1),(q1,b,q0)]
T2 = [(q0,c,q1),(q1,d,q0)]
T3 = [(q0,b,q1),(q1,c,q0),(q1,e,q0),(q0,d,q2),(q2,e,q0)]
T4 = [(q0,b,q1),(q1,c,q0),(q0,e,q0)]
SC=[a,b,c,d,e]
M1 = fsa(X_12,Sigma1,T1,X0,Xm,Sigcon=SC,name='$Maquina1$') 

M2 = fsa(X_12,Sigma2,T2,X0,Xm,Sigcon=SC ,name='$M_2$') 

AGV = fsa(X3,Sigma3,T3,X0,Xm,Sigcon=SC,name='$Robot$')

E = fsa(X_12,Sigma4,T4,X0,Xm,Sigcon=SC,name='$E$')


fabrica=M1//M2//AGV
#G.set(name='$G$',type='result')
H = fabrica//E
H.setpar(name='$H_{spec}$')
Ksup = supcontrollable(H,fabrica)
Ksup = Ksup.renamestates('number')
Ksup= Ksup.setpar(name =r'$K^{\uparrow}^C$')
K1=Ksup.addevent('h')
K1=Ksup.addevent('i')
draw(H,AGV,E,K1,Ksup,fabrica,'figure')
